$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $T$:Type.
\\[0ex]\{$m$:Msg$\mid$ source(mlnk($m$)) $=$ source($l$) $\in$ Id \}
\\[0ex]$\subseteq\rho$ Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{2}$ ${\it tg'}$ = ${\it tg}$$\rightarrow$ $T$ else Top fi)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ lnk($e$) $=$ $l$ $\Rightarrow$ tag($e$) $=$ ${\it tg}$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)